<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>

<title>ContractCheckingGenerator (randoop 4.1.0 API)</title>

<link rel="stylesheet" type="text/css" href="../../javadocstyle.css" title="Style">
<script type="text/javascript" src="../../script.js"></script>
</head>
<body>
<script type="text/javascript"><!--
    try {
        if (location.href.indexOf('is-external=true') == -1) {
            parent.document.title="ContractCheckingGenerator (randoop 4.1.0 API)";
        }
    }
    catch(err) {
    }
//-->
var methods = {"i0":10,"i1":10,"i2":9,"i3":10,"i4":9};
var tabs = {65535:["t0","All Methods"],1:["t1","Static Methods"],2:["t2","Instance Methods"],8:["t4","Concrete Methods"]};
var altColor = "altColor";
var rowColor = "rowColor";
var tableTab = "tableTab";
var activeTableTab = "activeTableTab";
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar.top">
<!--   -->
</a>
<div class="skipNav"><a href="#skip.navbar.top" title="Skip navigation links">Skip navigation links</a></div>
<a name="navbar.top.firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../randoop/test/CompilableTestPredicate.html" title="class in randoop.test"><span class="typeNameLink">Prev&nbsp;Class</span></a></li>
<li><a href="../../randoop/test/ContractSet.html" title="class in randoop.test"><span class="typeNameLink">Next&nbsp;Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?randoop/test/ContractCheckingGenerator.html" target="_top">Frames</a></li>
<li><a href="ContractCheckingGenerator.html" target="_top">No&nbsp;Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All&nbsp;Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field.summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor.summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method.summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field.detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor.detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method.detail">Method</a></li>
</ul>
</div>
<a name="skip.navbar.top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">randoop.test</div>
<h2 title="Class ContractCheckingGenerator" class="title">Class ContractCheckingGenerator</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li><a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true" title="class or interface in java.lang">java.lang.Object</a></li>
<li>
<ul class="inheritance">
<li><a href="../../randoop/test/TestCheckGenerator.html" title="class in randoop.test">randoop.test.TestCheckGenerator</a></li>
<li>
<ul class="inheritance">
<li>randoop.test.ContractCheckingGenerator</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public final class <span class="typeNameLabel">ContractCheckingGenerator</span>
extends <a href="../../randoop/test/TestCheckGenerator.html" title="class in randoop.test">TestCheckGenerator</a></pre>
<div class="block">An execution visitor that generates checks for error-revealing tests.

 <p>If execution of the visited sequence is normal, it will generate checks for contracts over the
 values from the execution. Contracts will be checked on all values except for boxed primitives or
 Strings. For each contract violation, the visitor adds a <code>Check</code> to the <code>TestChecks</code>
 object that is returned.

 <p>If the execution throws an exception considered to be an error, the visitor generates a <code>NoExceptionCheck</code> indicating that the statement should not throw the exception.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field.summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="memberSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>private <a href="../../randoop/test/ContractSet.html" title="class in randoop.test">ContractSet</a></code></td>
<td class="colLast"><code><span class="memberNameLink"><a href="../../randoop/test/ContractCheckingGenerator.html#contracts">contracts</a></span></code>&nbsp;</td>
</tr>
</table>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor.summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="memberSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><span class="memberNameLink"><a href="../../randoop/test/ContractCheckingGenerator.html#ContractCheckingGenerator-randoop.test.ContractSet-">ContractCheckingGenerator</a></span>(<a href="../../randoop/test/ContractSet.html" title="class in randoop.test">ContractSet</a>&nbsp;contracts)</code>
<div class="block">Create a new visitor that checks the given contracts after the last statement in a sequence is
 executed.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method.summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="memberSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span id="t0" class="activeTableTab"><span>All Methods</span><span class="tabEnd">&nbsp;</span></span><span id="t1" class="tableTab"><span><a href="javascript:show(1);">Static Methods</a></span><span class="tabEnd">&nbsp;</span></span><span id="t2" class="tableTab"><span><a href="javascript:show(2);">Instance Methods</a></span><span class="tabEnd">&nbsp;</span></span><span id="t4" class="tableTab"><span><a href="javascript:show(8);">Concrete Methods</a></span><span class="tabEnd">&nbsp;</span></span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr id="i0" class="altColor">
<td class="colFirst"><code>(package private) <a href="../../randoop/test/Check.html" title="interface in randoop.test">Check</a></code></td>
<td class="colLast"><code><span class="memberNameLink"><a href="../../randoop/test/ContractCheckingGenerator.html#checkContracts-java.util.List-randoop.sequence.ExecutableSequence-randoop.util.TupleSet-">checkContracts</a></span>(<a href="https://docs.oracle.com/javase/8/docs/api/java/util/List.html?is-external=true" title="class or interface in java.util">List</a>&lt;<a href="../../randoop/contract/ObjectContract.html" title="class in randoop.contract">ObjectContract</a>&gt;&nbsp;contracts,
              <a href="../../randoop/sequence/ExecutableSequence.html" title="class in randoop.sequence">ExecutableSequence</a>&nbsp;eseq,
              <a href="../../randoop/util/TupleSet.html" title="class in randoop.util">TupleSet</a>&lt;<a href="../../randoop/sequence/ReferenceValue.html" title="class in randoop.sequence">ReferenceValue</a>&gt;&nbsp;tuples)</code>
<div class="block">If a contract fails for some tuple, returns some such failing check.</div>
</td>
</tr>
<tr id="i1" class="rowColor">
<td class="colFirst"><code><a href="../../randoop/test/TestChecks.html" title="interface in randoop.test">TestChecks</a>&lt;?&gt;</code></td>
<td class="colLast"><code><span class="memberNameLink"><a href="../../randoop/test/ContractCheckingGenerator.html#generateTestChecks-randoop.sequence.ExecutableSequence-">generateTestChecks</a></span>(<a href="../../randoop/sequence/ExecutableSequence.html" title="class in randoop.sequence">ExecutableSequence</a>&nbsp;eseq)</code>
<div class="block">Generate a <a href="../../randoop/test/TestChecks.html" title="interface in randoop.test"><code>TestChecks</code></a> object for the executed sequence <code>eseq</code> based on the
 criteria of this generator.</div>
</td>
</tr>
<tr id="i2" class="altColor">
<td class="colFirst"><code>private static <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true" title="class or interface in java.lang">Object</a>[]</code></td>
<td class="colLast"><code><span class="memberNameLink"><a href="../../randoop/test/ContractCheckingGenerator.html#getValues-java.util.List-">getValues</a></span>(<a href="https://docs.oracle.com/javase/8/docs/api/java/util/List.html?is-external=true" title="class or interface in java.util">List</a>&lt;<a href="../../randoop/sequence/ReferenceValue.html" title="class in randoop.sequence">ReferenceValue</a>&gt;&nbsp;tuple)</code>
<div class="block">Creates an <code>Object</code> array for the given value list.</div>
</td>
</tr>
<tr id="i3" class="rowColor">
<td class="colFirst"><code>private <a href="../../randoop/test/TestChecks.html" title="interface in randoop.test">TestChecks</a>&lt;?&gt;</code></td>
<td class="colLast"><code><span class="memberNameLink"><a href="../../randoop/test/ContractCheckingGenerator.html#singletonTestCheck-randoop.test.Check-">singletonTestCheck</a></span>(<a href="../../randoop/test/Check.html" title="interface in randoop.test">Check</a>&nbsp;check)</code>
<div class="block">Return a TestChecks that contains only the given check.</div>
</td>
</tr>
<tr id="i4" class="altColor">
<td class="colFirst"><code>static boolean</code></td>
<td class="colLast"><code><span class="memberNameLink"><a href="../../randoop/test/ContractCheckingGenerator.html#typesMatch-randoop.types.TypeTuple-java.util.List-">typesMatch</a></span>(<a href="../../randoop/types/TypeTuple.html" title="class in randoop.types">TypeTuple</a>&nbsp;inputTypes,
          <a href="https://docs.oracle.com/javase/8/docs/api/java/util/List.html?is-external=true" title="class or interface in java.util">List</a>&lt;<a href="../../randoop/sequence/ReferenceValue.html" title="class in randoop.sequence">ReferenceValue</a>&gt;&nbsp;valueTuple)</code>
<div class="block">Indicates whether the given list of values matches the types in the type tuple.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods.inherited.from.class.randoop.test.TestCheckGenerator">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;randoop.test.<a href="../../randoop/test/TestCheckGenerator.html" title="class in randoop.test">TestCheckGenerator</a></h3>
<code><a href="../../randoop/test/TestCheckGenerator.html#hasGenerator-java.lang.Class-">hasGenerator</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods.inherited.from.class.java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.<a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true" title="class or interface in java.lang">Object</a></h3>
<code><a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#clone--" title="class or interface in java.lang">clone</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#equals-java.lang.Object-" title="class or interface in java.lang">equals</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#finalize--" title="class or interface in java.lang">finalize</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#getClass--" title="class or interface in java.lang">getClass</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#hashCode--" title="class or interface in java.lang">hashCode</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#notify--" title="class or interface in java.lang">notify</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#notifyAll--" title="class or interface in java.lang">notifyAll</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#toString--" title="class or interface in java.lang">toString</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#wait--" title="class or interface in java.lang">wait</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#wait-long-" title="class or interface in java.lang">wait</a>, <a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true#wait-long-int-" title="class or interface in java.lang">wait</a></code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field.detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="contracts">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>contracts</h4>
<pre>private&nbsp;<a href="../../randoop/test/ContractSet.html" title="class in randoop.test">ContractSet</a> contracts</pre>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor.detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ContractCheckingGenerator-randoop.test.ContractSet-">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ContractCheckingGenerator</h4>
<pre>public&nbsp;ContractCheckingGenerator(<a href="../../randoop/test/ContractSet.html" title="class in randoop.test">ContractSet</a>&nbsp;contracts)</pre>
<div class="block">Create a new visitor that checks the given contracts after the last statement in a sequence is
 executed.</div>
<dl>
<dt><span class="paramLabel">Parameters:</span></dt>
<dd><code>contracts</code> - expected to be unary contracts, i.e. for each contract <code>c</code>, <code>c.getArity() == 1</code>.</dd>
</dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method.detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="generateTestChecks-randoop.sequence.ExecutableSequence-">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>generateTestChecks</h4>
<pre>public&nbsp;<a href="../../randoop/test/TestChecks.html" title="interface in randoop.test">TestChecks</a>&lt;?&gt;&nbsp;generateTestChecks(<a href="../../randoop/sequence/ExecutableSequence.html" title="class in randoop.sequence">ExecutableSequence</a>&nbsp;eseq)</pre>
<div class="block">Generate a <a href="../../randoop/test/TestChecks.html" title="interface in randoop.test"><code>TestChecks</code></a> object for the executed sequence <code>eseq</code> based on the
 criteria of this generator.

 <p>Adds checks to final statement of sequence. Looks for failure exceptions, and violations of
 contracts in <code>contracts</code>.</div>
<dl>
<dt><span class="overrideSpecifyLabel">Specified by:</span></dt>
<dd><code><a href="../../randoop/test/TestCheckGenerator.html#generateTestChecks-randoop.sequence.ExecutableSequence-">generateTestChecks</a></code>&nbsp;in class&nbsp;<code><a href="../../randoop/test/TestCheckGenerator.html" title="class in randoop.test">TestCheckGenerator</a></code></dd>
<dt><span class="paramLabel">Parameters:</span></dt>
<dd><code>eseq</code> - the sequence for which checks are generated</dd>
<dt><span class="returnLabel">Returns:</span></dt>
<dd>the generated check set for the sequence</dd>
</dl>
</li>
</ul>
<a name="singletonTestCheck-randoop.test.Check-">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>singletonTestCheck</h4>
<pre>private&nbsp;<a href="../../randoop/test/TestChecks.html" title="interface in randoop.test">TestChecks</a>&lt;?&gt;&nbsp;singletonTestCheck(<a href="../../randoop/test/Check.html" title="interface in randoop.test">Check</a>&nbsp;check)</pre>
<div class="block">Return a TestChecks that contains only the given check.</div>
<dl>
<dt><span class="paramLabel">Parameters:</span></dt>
<dd><code>check</code> - the sole member of the singleton TestChecks</dd>
<dt><span class="returnLabel">Returns:</span></dt>
<dd>a TestChecks that contains only the given check</dd>
</dl>
</li>
</ul>
<a name="checkContracts-java.util.List-randoop.sequence.ExecutableSequence-randoop.util.TupleSet-">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>checkContracts</h4>
<pre><a href="../../randoop/test/Check.html" title="interface in randoop.test">Check</a>&nbsp;checkContracts(<a href="https://docs.oracle.com/javase/8/docs/api/java/util/List.html?is-external=true" title="class or interface in java.util">List</a>&lt;<a href="../../randoop/contract/ObjectContract.html" title="class in randoop.contract">ObjectContract</a>&gt;&nbsp;contracts,
                     <a href="../../randoop/sequence/ExecutableSequence.html" title="class in randoop.sequence">ExecutableSequence</a>&nbsp;eseq,
                     <a href="../../randoop/util/TupleSet.html" title="class in randoop.util">TupleSet</a>&lt;<a href="../../randoop/sequence/ReferenceValue.html" title="class in randoop.sequence">ReferenceValue</a>&gt;&nbsp;tuples)</pre>
<div class="block">If a contract fails for some tuple, returns some such failing check.</div>
<dl>
<dt><span class="paramLabel">Parameters:</span></dt>
<dd><code>contracts</code> - the contracts to check</dd>
<dd><code>eseq</code> - the executable sequence that is the source of values for checking contracts</dd>
<dd><code>tuples</code> - the value tuples to use as input to the contracts</dd>
<dt><span class="returnLabel">Returns:</span></dt>
<dd>a <a href="../../randoop/test/Check.html" title="interface in randoop.test"><code>Check</code></a> of the first contract+tuple that did not succeed, or null if all
     contracts succeeded. More specifically, returns a <a href="../../randoop/test/ObjectCheck.html" title="class in randoop.test"><code>ObjectCheck</code></a> if a contract fails,
     an <a href="../../randoop/test/InvalidExceptionCheck.html" title="class in randoop.test"><code>InvalidExceptionCheck</code></a> if a contract throws an exception indicating that the
     sequence is invalid, null otherwise.</dd>
</dl>
</li>
</ul>
<a name="typesMatch-randoop.types.TypeTuple-java.util.List-">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>typesMatch</h4>
<pre>public static&nbsp;boolean&nbsp;typesMatch(<a href="../../randoop/types/TypeTuple.html" title="class in randoop.types">TypeTuple</a>&nbsp;inputTypes,
                                 <a href="https://docs.oracle.com/javase/8/docs/api/java/util/List.html?is-external=true" title="class or interface in java.util">List</a>&lt;<a href="../../randoop/sequence/ReferenceValue.html" title="class in randoop.sequence">ReferenceValue</a>&gt;&nbsp;valueTuple)</pre>
<div class="block">Indicates whether the given list of values matches the types in the type tuple. Contracts may
 have generic input types, so this method checks for consistent substitutions across value
 types.</div>
<dl>
<dt><span class="paramLabel">Parameters:</span></dt>
<dd><code>inputTypes</code> - the expected types for contract input</dd>
<dd><code>valueTuple</code> - the values to match against input types</dd>
<dt><span class="returnLabel">Returns:</span></dt>
<dd>true if the types of the values are assignable to the expected types, false otherwise</dd>
</dl>
</li>
</ul>
<a name="getValues-java.util.List-">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>getValues</h4>
<pre>private static&nbsp;<a href="https://docs.oracle.com/javase/8/docs/api/java/lang/Object.html?is-external=true" title="class or interface in java.lang">Object</a>[]&nbsp;getValues(<a href="https://docs.oracle.com/javase/8/docs/api/java/util/List.html?is-external=true" title="class or interface in java.util">List</a>&lt;<a href="../../randoop/sequence/ReferenceValue.html" title="class in randoop.sequence">ReferenceValue</a>&gt;&nbsp;tuple)</pre>
<div class="block">Creates an <code>Object</code> array for the given value list.</div>
<dl>
<dt><span class="paramLabel">Parameters:</span></dt>
<dd><code>tuple</code> - the list of values</dd>
<dt><span class="returnLabel">Returns:</span></dt>
<dd>the Object array for the values</dd>
</dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar.bottom">
<!--   -->
</a>
<div class="skipNav"><a href="#skip.navbar.bottom" title="Skip navigation links">Skip navigation links</a></div>
<a name="navbar.bottom.firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../randoop/test/CompilableTestPredicate.html" title="class in randoop.test"><span class="typeNameLink">Prev&nbsp;Class</span></a></li>
<li><a href="../../randoop/test/ContractSet.html" title="class in randoop.test"><span class="typeNameLink">Next&nbsp;Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?randoop/test/ContractCheckingGenerator.html" target="_top">Frames</a></li>
<li><a href="ContractCheckingGenerator.html" target="_top">No&nbsp;Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All&nbsp;Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field.summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor.summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method.summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field.detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor.detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method.detail">Method</a></li>
</ul>
</div>
<a name="skip.navbar.bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
